$\forall$$A$:Type, $f$:fpf($A$; $x$.top). fpf{-}is{-}empty($f$) $\in$ $\mathbb{B}$